COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.at "∪"⊂"↓_"⊃  
C00008 ENDMK
C⊗;
.at "∪"⊂"↓_"⊃  
.at "∩"⊂"_↓"⊃  
.turn on "↓_";
.Sec(Bibliography,,)
.begin indent 0,12;
[1]####Allen, John, R.  ∪Anatomy of LISP∩.  To be published by McGraw-Hill
Publishing Co., New York, New York, 1977.
####################################################################################

[2]####Gordon, M. J. C.  "Models of Pure LISP".  Ph.D. dissertation, School of Artificial Intelligence,
University of
Edinburgh, 1973.
###################################################################################

[3]####Kleene, Stephen Cole.  ∪Introduction to Metamathematics∩.  New York, New
York: D. Van Nostrand Company, Inc., 1952.
###################################################################################

[4]####Kowalski, R. A. and M. H. van Emden.  "The Semantics of Predicate Logic
as a Programming Language".  Memorandum, School of Artificial Intelligence,
University of Edinburgh, 1974.
###################################################################################

[5]####Loveland, D.  "Seminar on Mechanical Theorem-Proving: First Order Proof
Procedures".  Lecture Notes, Carnegie-Mellon University, 1972.
####################################################################################

[6]####Luckham, David.  "The Resolution Principle in Theorem Proving," ∪Machine
Intelligence∩, Vol. I.  New York, New York: American Elsevier, 1966.
#####################################################################################

[7]####Lyndon, Roger C.  ∪Notes on Logic∩.  Princeton, New Jersey: D. Van Nostrand
Company, Inc., 1966.
####################################################################################

[8]####Mendelson, Elliott.  ∪Introduction to Mathematical Logic∩.  Princeton, New
Jersey: D. Van Nostrand Company, Inc., 1964.
####################################################################################


[9]####Milner, Robin.  "Logic for Computable Functions, Description of a Machine
Implementation," Memorandum, Stanford Artificial Intelligence Project, Stanford
University, 1972.
####################################################################################


[10]####Milner, Robin. "Models of LCF", Memorandum, Stanford Artificial Intelligence
 Project, Stanford University, 1973.
####################################################################################


[11]####Plotkin, Gordon D.  "LCF Considered as a Programming Language", Memorandum,
School of Artificial Intelligence, University of Edinburgh, 1974.
####################################################################################


[12]####Scott, Dana.  "A Type-Theoretical Alternative to CUCH, ISWIM, OWHY%8*%1
(%8*%1Or What Have You)", Unpublished memorandum, Oxford, 1969.
####################################################################################


[13]####Scott, Dana.  "Models for Various Type-Free Calculi", ∪Logic, Methodology
and∩ ∪Philosophy∩,Vol. IV, pp.157-187.  P. Suppes et al., eds.,North Holland Publishing Company, 1973.
####################################################################################


[14]####Thompson, Frederick B.  "Symbolic Logic", Lecture Notes, University of
California, Santa Barbara, 1964.
####################################################################################


[15]####Wadsworth, Christopher P.  "SIS 830: Lambda Calculus", Lecture Notes,
Syracuse University, 1974.
.end